$\forall$$T$, ${\it T'}$:Type, $x$:Id, $c$:$T$, $a$:Id, $P$:($T$$\rightarrow$${\it T'}$$\rightarrow$Prop).
\\[0ex]${\it T'}$
\\[0ex]$\Rightarrow$ ($\forall$$u$:$T$. Dec($\exists$$v$:${\it T'}$. $P$($u$,$v$)))
\\[0ex]$\Rightarrow$ AtomFree(Type;$T$)
\\[0ex]$\Rightarrow$ AtomFree(Type;${\it T'}$)
\\[0ex]$\Rightarrow$ Feasible(ma{-}single{-}pre{-}init1($x$;$T$;$c$;$a$;${\it T'}$;$x$,$v$.$P$($x$,$v$)))